Type Inference
Static typing has advantages for safety, speed, and documentation, but it often requires manual type annotations. In this seminar, we look at approaches to type checking that reduce the need for annotations.
In particular, the Damas-Milner algorithm always infers the most general type without any type annotations, and is used in practical languages like OCaml. However, it only works for a suitably restricted type system. In more powerful type system, type inference can become much more complex. A promising approach is bidirectional typing, which combines type checking and inference into one procedure. While it does not fully get rid of annotations like Damas-Milner, it reduces the need for annotations while being easier to implement and scaling to more complex type systems.
In the seminar, you will look at and compare different approaches to typing. You will also write toy programs in a language with type inference (e.g. Haskell, OCaml) to probe the strengths and limitations of the approach.
In the project, you will implement a type checker/inference for an advanced type system, e.g. the calculus of inductive constructions or first-class polymorphism (see References).